@PhDThesis{Santos:2015:MeApFo,
author = "Santos, Luciana Brasil Rebelo dos",
title = "A methodology to apply formal verification to UML-based software",
school = "Instituto Nacional de Pesquisas Espaciais (INPE)",
year = "2015",
address = "S{\~a}o Jos{\'e} dos Campos",
month = "2015-10-02",
keywords = "UML, formal verification, model checking, SOLIMVA, formal methods,
verifica{\c{c}}{\~a}o formal, m{\'e}todos formais.",
abstract = "Software development organizations aim to add quality to the
created products, especially those dealing with critical systems,
which require high quality software. Formal Methods offer a large
potential to provide more effective verification techniques.
Besides, Formal Verification methods, such as Model Checking, are
best applied in early stages of system design, when costs are low
and benefits can be high, increasing the quality of systems.
Unified Modeling Language (UML) is widely used for modeling
(object-oriented) software, and its use is increasing in the
aerospace industry. Verification and Validation of complex
software developed according to UML is not trivial due to
complexity of the software itself, and the several different UML
models/diagrams that can be used to model behavior and structure
of the software. This PhD thesis presents an extension of a
methodology called SOLIMVA, initially developed to generate
model-based system and acceptance test cases considering Natural
Language requirements artifacts (SOLIMVA 1.0), and to detect
incompleteness in software specifications by means of Model
Checking (SOLIMVA 2.0). Such an extension generated SOLIMVA 3.0
which transforms up to three different UML behavioral diagrams
(sequence, behavioral state machine, and activity) into a single
Transition System to support Model Checking of software developed
in accordance with UML. In SOLIMVA 3.0, properties are formalized
based on use case models or requirements expressed in pure textual
notation. The translation into the Transition System is done for
the NuSMV model checker, but there is a possibility in using other
model checkers, such as SPIN. A tool, XML Metadata Interchange to
Transition System (XMITS), was developed to automate some steps of
SOLIMVA 3.0 methodology. The approach was applied to two real case
studies (embedded software) related to project under development
at Instituto Nacional de Pesquisas Espaciais (INPE). Defects were
detected within the design of these software systems showing the
feasibility of the methodology. The main contribution of this PhD
thesis is the transformation of a non-formal language (UML) to a
formal language (language of the NuSMV model checker) towards a
greater adoption in practice of Formal Methods in software
development. RESUMO: Organiza{\c{c}}{\~o}es que desenvolvem
software objetivam produzir produtos de software de qualidade,
especialmente aquelas que lidam com sistemas cr{\'{\i}}ticos,
que demandam software de alta qualidade. M{\'e}todos Formais
oferecem grande potencial para prover t{\'e}cnicas de
verifica{\c{c}}{\~a}o mais efetivas. Al{\'e}m disso,
m{\'e}todos de Verifica{\c{c}}{\~a}o Formal, como Model
Checking, s{\~a}o aplicados de maneira mais eficiente nos
est{\'a}gios iniciais do projeto de software, quando os custos
ainda s{\~a}o baixos e os benef{\'{\i}}cios podem ser altos,
aumentando a qualidade dos sistemas de software. A Linguagem de
Modelagem Unificada (UML) {\'e} consideravelmente utilizada para
modelar software (orientado a objetos), e seu uso tem crescido na
ind{\'u}stria aeroespacial. Verifica{\c{c}}{\~a}o e
Valida{\c{c}}{\~a}o de sistemas complexos desenvolvidos de
acordo com UML n{\~a}o s{\~a}o tarefas triviais, devido {\`a}
complexidade do software em si, e a diversos diagramas/modelos UML
diferentes que podem ser usados para modelar o comportamento e a
estrutura do sistema. Esta tese de doutorado apresenta uma
extens{\~a}o de uma metodologia chamada SOLIMVA, desenvolvida
inicialmente para gerar casos de teste de sistema e de
aceita{\c{c}}{\~a}o baseados em modelos, considerando requisitos
em Linguagem Natural (SOLIMVA 1.0), e para detectar n{\~a}o
completude em especifica{\c{c}}{\~o}es de software utilizando
Model Checking (SOLIMVA 2.0). Tal extens{\~a}o gerou a SOLIMVA
3.0, a qual transforma at{\'e} tr{\^e}s diferentes diagramas
comportamentais da UML (sequ{\^e}ncia, atividades e m{\'a}quina
de estado) em um {\'u}nico Sistema de Transi{\c{c}}{\~a}o de
Estados para possibilitar a aplica{\c{c}}{\~a}o de Model
Checking em software desenvolvido de acordo com a UML. Na SOLIMVA
3.0, as propriedades s{\~a}o formalizadas baseando-se nos modelos
de casos de uso ou em requisitos expressos em nota{\c{c}}{\~a}o
textual pura. A tradu{\c{c}}{\~a}o para o Sistema de
Transi{\c{c}}{\~a}o de Estados {\'e} feita para a ferramenta de
Model Checking NuSMV, mas existe a possibilidade de se utilizar
outras ferramentas, como por exemplo, SPIN. Uma ferramenta, XML
Metadata Interchange to Transition System (XMITS), foi
desenvolvida para automatizar algumas atividades da metodologia
SOLIMVA 3.0. A abordagem foi aplicada em dois estudos de caso
reais (software embarcado) relacionados a um projeto em
desenvolvimento no Instituto Nacional de Pesquisas Espaciais
(INPE). Foram encontrados defeitos nos projetos desses sistemas de
software, mostrando a viabilidade da metodologia. A principal
contribui{\c{c}}{\~a}o desta tese de doutorado {\'e} a
transforma{\c{c}}{\~a}o de uma linguagem n{\~a}o formal (UML)
para uma linguagem formal (linguagem de entrada da ferramenta de
Model Checking NuSMV), tendo como objetivo uma maior
utiliza{\c{c}}{\~a}o, na pr{\'a}tica, de M{\'e}todos Formais
no processo de desenvolvimento de software.",
committee = "Carvalho, Solon Ven{\^a}ncio de (presidente) and Santiago
J{\'u}nior, Valdivino Alexandre de (orientador) and Vijaykumar,
Nandamudi Lankalapalli (orientador) and Silveira, F{\'a}bio
Fagundes and Yano, Edgar Toshiro",
copyholder = "SID/SCD",
englishtitle = "Uma metodologia para aplicar verifica{\c{c}}{\~a}o formal a
software desenvolvido de acordo com UML",
language = "en",
pages = "196",
ibi = "8JMKD3MGP3W34P/3K7T2BB",
url = "http://urlib.net/ibi/8JMKD3MGP3W34P/3K7T2BB",
targetfile = "publicacao.pdf",
urlaccessdate = "27 abr. 2024"
}